package agent.ccs
//import agent._
import scala.collection.mutable.Seq
import java.util.ArrayList
import scala.collection.mutable.LinkedList
import scala.collection.mutable.HashMap
import com.sun.org.apache.xalan.internal.xsltc.compiler.ForEach
import cwb.Panic
import scala.collection.SortedSet
import cwb.Error
import agent.Agent
import agent.AgentObject
import agent.Action



case class CCSAgent(privAgent: PrivateAgent, word: Int) extends Agent {
  type Transition = CCSAgent.Transition
  type ComponentTransitionList = List[(List[Transition], CCSAgent)]
  
  def agentString: String = privAgent.agentString
  
  
  /**
   * printAgent prints the string representation of the agent.
   */
  def printAgent() = print(agentString)
  
  
  /**
   * CCSAgents are equal if their private agents are the same.
   */
  override
  def equals(obj: Any): Boolean = {
    obj match {
      case ag: CCSAgent => ag.asInstanceOf[CCSAgent].privAgent == privAgent
      case _ => false
    }
  }
  
  override
  def hashCode() = privAgent.hashCode()
  
  def diverges(): Boolean = {
     privAgent.diverges()
  }
  


  def transitions(): List[Transition] = {
    val trans: List[Transition] = CCSAgent.transitions(this)
    // Sort TODO (figure out if this needs to be done before)
    trans.sortBy(_._1)
  }
  
    def printTransitions() = {
      for ((act, ag) <- transitions()) yield println(CCSAgent.transitionString(act, ag)) 
    }
}

object CCSAgent extends AgentObject {
  type Transition = (CCSAction, CCSAgent)
  type ComponentTransitionList = List[(List[Transition], CCSAgent)]
  type LiteralRelabelling = HashMap[Symbol, Act]
  

  private val knowledge = new HashMap[CCSAgent, List[Transition]]
  private var total = 0
  private var madeNew = 0
  
  private var agents = new HashMap[Symbol, PrivateAgent]

  /**
   * Wraps a private agent inside a new CCSAgent.
   * @param p, private agent to be wrapped
   * @return a CCSAgent corresponding to the given private agent.
   */
  def makeAgent(p: PrivateAgent): CCSAgent = {
    new CCSAgent(p, p.hashCode())
  }
  

  
  /**
   * checkForBadRecursion ensures the CWB does not get stuck in infinite variable
   * recursions such as agent A = A
   * @param varAg - The agent variable to be checked for bad recursion.
   */
  def checkForBadRecursion(varAg: PVar) = {
    val maxLookup = 2000
    var agent: CCSAgent = null
    try {
      agent = varAg.agent
    } catch {
      case e: Unbound => println("Agent " + varAg.s.name + " is unbound")
    }
    if (CCSComponent.environment.getAccesses(varAg.s) > maxLookup) {
      throw new Error("Non-well-founded recursion in " + varAg.s.name)
    }
  }
  
  /**
   * Outputs a string representation for the given transition
   * SML name: printders
   * @param trans transition to be represented as a string
   * @return the string representation of the given transition
   */
  def transitionString(trans: Transition): String = {
    trans match {
      case (act, ag) => "--- " + act.mkstr + " ---> " + ag.agentString
    }
  }
  
  
  /**
   * printTransList prints the string representation of the given transition.
   * @param trans list of transitions to be printed.
   */
  def printTransList(trans: List[(Action, Agent)]) = {
    // Sort the transitions before printing
   printListForAgent(transitionString, trans.asInstanceOf[List[Transition]].sortWith(transLE))
   
  }
  
  /**
   *  transLE sorts a pair of transitions with primary sort key act1 <= act2 and secondarily 
   *  based on the agents hash value.
   *  SML name: ts_le
   *  @param l first transition (lhs)
   *  @param r second transition (rhs)
   *  @return l <= r
   */
  def transLE(l: Transition, r: Transition) = {
    if (l._1 == r._1) l._2.hashCode() < r._2.hashCode() else l._1 < r._1  
  }

  /**
   * Prints a list of transitions using the given transition->string function to determine
   * the representation.
   * @param f function producing a string from a transition
   * @param transitions a list of transitions to be printed.
   * 
   */
  def printListForAgent(f: Transition => String, transitions: List[Transition]): Unit = {
    transitions match {
       case List() => println("None.")
       case _ => transitions.foreach(x => println(f(x)))
    }
  }
  
  
  
    /* use noTauOrigbecause if you're using this funnction you don't want taus to  */
  /* be labelled as resulting from synchronising on a: it'd be false. */
  def makeAgentFromNextSteps(l: List[(CCSAction, List[Symbol])]): CCSAgent = {


      // Original mktrans
      def makePVarPrefix(action: CCSAction, v: Symbol): CCSAgent = {
          makeAgent(new PPrefix(List(Prefix.prefixFromAction(action)), makeAgent(new PVar(v))))
      }

      // Original mkag
      def mkag(gen0: List[(CCSAction, List[Symbol])]): List[CCSAgent] = {
          gen0 match {
          case (List()) => {
            List()
          } case ((ac,lst)::t) => {
            (for (l<-lst) yield makePVarPrefix(ac, l)) ++ mkag(t)
          }
          }
      }
      /**
       * makeSumAgent takes a list of agents from which it composes a new agent.
       * If the list is empty it returns a new nil agent and otherwise the agents
       * are added as part of a sum agent.
       * SML name: mksum
       * @param agentList: List of agents to be combined into a sum agent.
       * @return a sum or a nil CCS agent.
       */
      def makeSumAgent(agentList: List[CCSAgent]): CCSAgent = {
          agentList match {
          case (List()) => {
            makeAgent(new PNil)
          } case (List(h)) => {
            h
          } case (l) => {
            makeAgent(new PSSum(l))

          }
          }
      }
      makeSumAgent(mkag(l))
  }

  

  /**
   * transitions returns a list of transitions for the given CCSAgent.
   * @param agent the agent whose transitions are to be looked up.
   * @return list of agent's transitions.
   */
  private def transitions(agent: CCSAgent): List[Transition] =  {
    def mv(compDone: List[CCSAgent], trans: List[Transition],
        compRemaining: ComponentTransitionList): List[Transition] = {

      (compDone, trans, compRemaining) match {

        
        // (* if there aren't any components, there aren't any transitions *)
        case (_, Nil, Nil) => List()
        // (* if there's only one component and it hasn't any transitions, ditto *)
        case (_, Nil, List(_)) => List()
        
        /* if this component has no transitions, no more to be done with it,  *)
        (* add it to collection of components we've done and keep going with rest */
        case (left, Nil,(_,a)::(t@(l,_)::_)) => mv(left ++ List(a), l, t)
        
        // This component does have transitions so do the real work here
        case (left, a@(ac,ag)::t, right@(_::rt)) => {
          def comm(xs: List[CCSAgent], ys: List[Transition],
                   zs: ComponentTransitionList): List[Transition] = {

            (xs, ys, zs) match {
              case (_, Nil, Nil) => List()
              case (_, Nil, List(_)) => List()
              case (chk, Nil,(_,a)::(t@(l,_)::_)) => comm(chk ++ List(a), l, t)
              
              case (chk, b@(bc,bg)::u, (cright@_::ct)) => { 
                CCSAction.inverses(ac, bc) match {
                  // No synchronisation.
                  case None => comm(chk, u, cright)

                  case Some((agIsSender, resultant, receiverConstraint)) => {
                    // TODO(gustafa): Add constraints see source file
                    val (newA, newB) = 
                      receiverConstraint match {
                      case None => (ag, bg)
                      //case Some(e) => s. Must add constraints!
                    }
                    List((resultant, CCSAgent.makeAgent(
                        (new PParallel(left ++ (List(newA) ++ chk) ++
                            (List(newB) ++ (for (c <- ct) yield c._2))))))) ++ comm(chk, u, cright)
                  }
                }
             }
              case _ => throw Panic("Shouldn't happen! Comm reached") 
            }
            
          }

          // TODO(gustafa): Combine comms and this lot for increased efficiency
          val comms: List[Transition] = if (ac.getClass() == classOf[Tau] || rt == Nil) List()
                      else comm(List(), rt.first._1, rt)
          
          val thisLot: List[Transition] = comms :+ (ac, CCSAgent.makeAgent(new PParallel(left ++ List(ag) ++
              (for ((cact, cgent) <- rt) yield cgent))))
          
          var finalList = thisLot ++ mv(left,t,right)
          finalList sort {(l, r) => 
            // TODO(Gustafa): Evaluate
            if (l._1 == r._1) l._2.hashCode() < r._2.hashCode() else l._1 < r._1 
          }
          finalList
        }
        case _ => throw Panic("MV, shouldn't happen!")
      }
      
    } 
    
    def expand(ls: ComponentTransitionList) = {
      ls match {
        case Nil => List() 
        case (l, _)::_ => mv(List(), l, ls)
      }
    }
    
    def ts(chk: List[CCSAgent], ag: CCSAgent): List[Transition] = {
      ts2(chk, ag.privAgent)
    }
    
    /**
     * 
     */
    def tsifnec(chk: List[CCSAgent], ag: CCSAgent): List[Transition] = {
      total += 1
      
      knowledge.get(agent) match {
        case Some(x) => x
        case None => {
          val calculated = ts(chk, ag)
          madeNew += 1
          knowledge.put(agent, calculated)
          calculated
        }
      }
      
      
      // TODO: Add hashmap for quicker computation
    val trans = ts2(chk, ag.privAgent)
      trans
    }
    
    def relabelAction(litRel: HashMap[Symbol, Act], action: CCSAction): CCSAction = {
      // Simply return if it's not an act. TODO: Add Tau?
      if (action.getClass != classOf[Act]) return action
      
      val act = action.asInstanceOf[Act]
      litRel.get(act.port) match {
        case None => act
        case Some(x) => {
          act.change(x)
        }
      }
    }
    
    def relabel(agent: CCSAgent, rel: Relabeling): CCSAgent = {//HashMap[Symbol, Act]): CCSAgent = {
      val litRel = rel.getMap
        if (litRel.size == 0) agent else makeAgent(new PRelabel(agent, rel))
    }

    // chk provisional
    def ts2(chk: List[CCSAgent], pag: PrivateAgent): List[Transition] = {
      pag match {
        case (p: PNil) => List()
        case (p: PPrefix) =>
          val ls = p.prefixes
 
          
          if (ls.size == 1) {
            List((ls(0).toAct(),  p.agent))
          } else {
          // TODO(gustafa): Hack! What is going on?
          ls match {
            case (h::t) => List((h.toAct(), CCSAgent.makeAgent(PPrefix(t, p.asInstanceOf[PPrefix].agent))))
            case _ => throw Panic("TS2, unexpected empty Prefix encountered")
          }
        
        }
        case (p: PRestrict) => {
          val rests = p.restriction
          // Grab inner agent transitions.
          val trans = tsifnec(chk, p.agent)
          //println("Trans before " + trans)
          var allowedTrans: List[Transition] = List()
          // Filter out the ones which are restricted.
          // ORG NAME: rmac
          def removeRestActs(ts: List[Transition]): List[Transition] = {
            ts match {
              case List() => allowedTrans
              case (act, ag)::as => {
                if (rests.allows(act)) {
                  allowedTrans = allowedTrans ++ List((act, makeAgent(new PRestrict(ag, rests))))
                }
                removeRestActs(as)
              } 
            }
          }
         removeRestActs(trans)
         return allowedTrans    
        }
        
        case (p: PSSum) => {
          // In the case of A + B the union of their transitions 
          var trans: List[Transition] = List()
          for (ag <- p.agents) {
            trans = trans ++ ag.transitions()
          }
          // Return the sorted concatenation

          val x = trans.sortWith(transLE).removeDuplicates
//          printTransList(x)

          x
        }
        case (p: PVar) => {
          checkForBadRecursion(p)
          tsifnec(chk, p.agent)
        }
        
        case (p: PParallel) => expand(for (x<-p.agents) yield (tsifnec(chk, x), x))
        
        case (p: PRelabel) => {
          //val relA = p.relabel.getMap
                    
          val res = for ((a, ag) <- tsifnec(chk, p.agent)) yield (relabelAction(p.relabel.getMap, a), relabel(ag, p.relabel))
          res.sort(transLE)
        }
      }
    }
    val trans = tsifnec(List(), agent)
    trans.sortWith(transLE)
  }
}